Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    a__2nd(cons(X,cons(Y,Z)))  → mark(Y)
2:    a__from(X)  → cons(mark(X),from(s(X)))
3:    mark(2nd(X))  → a__2nd(mark(X))
4:    mark(from(X))  → a__from(mark(X))
5:    mark(cons(X1,X2))  → cons(mark(X1),X2)
6:    mark(s(X))  → s(mark(X))
7:    a__2nd(X)  → 2nd(X)
8:    a__from(X)  → from(X)
There are 8 dependency pairs:
9:    A__2ND(cons(X,cons(Y,Z)))  → MARK(Y)
10:    A__FROM(X)  → MARK(X)
11:    MARK(2nd(X))  → A__2ND(mark(X))
12:    MARK(2nd(X))  → MARK(X)
13:    MARK(from(X))  → A__FROM(mark(X))
14:    MARK(from(X))  → MARK(X)
15:    MARK(cons(X1,X2))  → MARK(X1)
16:    MARK(s(X))  → MARK(X)
Consider the SCC {9-16}. The constraints could not be solved.
Tyrolean Termination Tool  (0.07 seconds)   ---  May 3, 2006